:- module(flog,
	  [ mi/1,
	    op(550, fx, '?'),
	    op(1150, xfx, ':='),
	    op(525, xfx, '~>'),
	    op(1000, xfy, '\\/'),
	    op(1100, xfy, '/\\' )
	      ]).

:- multifile ':='.

% All thunks in the first arg are variables in the second
thunk_vars(X, _) :-
	nonvar(X), X = ?_.
thunk_vars(X, _) :-
	var(X).
thunk_vars(X, Y) :-
	X \= ? _,
	X =.. [Name|XArgs],
	maplist(thunk_vars, XArgs, YArgs),
	Y =.. [Name|YArgs].

% unifies a thunk as a list, fails if this is not possible
thunk_as_list(Thunk, [], Ls, Ld) :-
	unify_lazy(Thunk, [], Ls, Ld).
thunk_as_list(Thunk, [H|Tail], Ls, Ld) :-
	unify_lazy(Thunk, [H|TailThunk], Ls, Lt),
	thunk_as_list(TailThunk, Tail, Lt, Ld).

% Gets a clause of the program, also evaluates built in goals
mi_clause(F =.. [N|A], Ls, Ld) :-
	thunk_as_list([N|A], [NN|AA], Ls, Ld),
	expand(NN, NNN),
	F =.. [NNN|AA].
mi_clause(F > L, Ld, Ld) :-
	expand(F, FF), expand(L, LL), FF > LL.
mi_clause(F >= L, Ld, Ld) :-
	expand(F, FF), expand(L, LL), FF >= LL.
mi_clause(F < L, Ld, Ld) :-
	expand(F, FF), expand(L, LL), FF < LL.
mi_clause(F =< L, Ld, Ld) :-
	expand(F, FF), expand(L, LL), FF =< LL.
mi_clause(F is L, Ld, Ld) :-
	expand(L, LL), F is LL.
mi_clause(X = Y, Ls, Ld) :-
	unify_lazy(X, Y, Ls, Ld).
mi_clause('~>'(N, L), [P|Ld], Ld) :-
	N =.. Args,
	append(Args, L, LL),
	P =.. LL.
mi_clause(writeln(X), L, L) :-
	expand(X, XX),
	write(XX), nl.
mi_clause(number(X), Ld, Ld) :-
	expand(X, XX), number(XX).
mi_clause(atom(X), Ld, Ld) :-
	expand(X, XX), atom(XX).
mi_clause(G, Ls, Ld) :-
	G \= (_ =.. _), G \= (_ < _),
	G \= (_ > _), G \= (_ >= _),
	G \= (_ =< _), G \= (_ is _),
	G \= (_ = _),
	G \= '~>'(_, _), G \= number(_), G \= atom(_),
	thunk_vars(G, GG),
	clause(GG, Body),
	unify_lazy(GG, G, Ls, Lt),
	phrase(body_list(Body), Lt, Ld).

expand(G, GG) :-
	(var(G); atom(G); number(G)),
	G = GG.
expand(?G, GG) :-
	eval(G, GG).
expand(G, GG) :-
	G \= ?_, \+ var(G),  \+ atom(G), \+ number(G),
	G =.. [Name|Args],
	maplist(expand, Args, A),
	GG =.. [Name|A].

body_list(true) --> [].
body_list(A /\ B) -->
	body_list(A),
	body_list(B).
body_list(A \/ B) -->
	body_list(A);
	body_list(B).
body_list(G) -->
	{ G \= true },
	{ G \= '/\\'(_, _) },
	{ G \= '\\/'(_, _) },
	[G].

thunk_list([], []).
thunk_list([H|T], [?H|TT]) :-
	H \= (?_),
	thunk_list(T, TT).
thunk_list([?H|T], [?H|TT]) :-
	thunk_list(T, TT).

thunk_args(X, Y) :-
	nonvar(X),
	X =.. [Name|Args],
	thunk_list(Args, AArgs),
	Y =.. [Name|AArgs].
thunk_args(X, Y) :-
	nonvar(Y),
	Y =.. [Name|AArgs],
	thunk_list(Args, AArgs),
	X =.. [Name|Args].

unify_lazy(X, Y, L, L) :-
	var(X),
	var(Y),
	X = Y.
unify_lazy(X, Y, L, L) :-
	var(X),
	nonvar(Y),
	X = Y.
unify_lazy(X, Y, L, L) :-
	nonvar(X),
	var(Y),
	X = Y.
unify_lazy(X, ? Y, Ls, Ld) :-
	nonvar(X), X \= ? _,
	nonvar(Y), thunk_args(Y, YY),
	(Ls = [(YY := YExp), X = YExp|Ld]; atomic(Y), Ls = [X = Y|Ld]).
unify_lazy(? X, Y, Ls, Ld) :-
	nonvar(Y), Y \= ? _,
	nonvar(X), thunk_args(X, XX),
	(Ls = [(XX := XExp), XExp = Y|Ld]; atomic(X), Ls = [X = Y|Ld]).
unify_lazy(? X, ? Y, Ls, Ld) :-
	nonvar(X), thunk_args(X, XX),
	nonvar(Y), thunk_args(Y, YY),
	(Ls = [(XX := XExp), (YY := YExp), YExp = XExp|Ld]; atomic(X), Ls = [X = ? Y|Ld]).
unify_lazy(X, Y, Ls, Ld) :-
	nonvar(X), X \= ? _,
	nonvar(Y), Y \= ? _,
	X =.. [Name|XArgs],
	Y =.. [Name|YArgs],
	unify_lazy_list(XArgs, YArgs, Ls, Ld).
unify_lazy_list([], [], Ls, Ls).
unify_lazy_list([XH|XT], [YH|YT], Ls, Ld) :-
	unify_lazy(XH, YH, Ls, Lt),
	unify_lazy_list(XT, YT, Lt, Ld).


eval(.(AA, BB), .(A, B)) :-
	eval(AA, A),
	eval(BB, B).
eval(?X, R) :-
	eval(X, R).
eval(Func, R) :-
	Func \= ?_,
	Func =.. [Name|Args],
	maplist(eval, Args, A),
	F =.. [Name|A],
	(mi_((F := RR)); atomic(F), F = RR),
	expand(RR, R).

mi_(G) :-
	phrase(body_list(G), GL, []),
	mi_list(GL).

mi(G) :-
	copy_term(G, GG),
	copy_term(G, GGG),
	mi_(GGG),
	free_variables(G, GL),
	free_variables(GG, GGL),
	GGG = GG,
	expand(GGL, GL).

mi_backtrack_([[]-G|_], G).
mi_backtrack_(Alts0, G) :-
	resstep_(Alts0, Alts1),
	mi_backtrack_(Alts1, G).

mi_list([]).
mi_list([G0|Gs0]) :-
	mi_clause(G0, Remaining, Gs0),
	mi_list(Remaining).

